effect system勉強会
Extensible Eff Applicative
「他の人がモナドの話をすると思ったので、私はアプリカティブの話をします」
code:haskell
e5 :: FreeAp (Exc String) Integer
e5 = Impure Ap (Exc "foo") $ ImpureAp (Exc "bar") $ Pure (+)
e6 :: Freer (Exc String) Integer
e6 = Impure (Exc "foo") $ \a -> Impure (Exc "bar") $ \b -> Pure (a + b)
applicativeの式は"foo"と"bar"両方を参照できる。
monadの式は"foo"のみ取得でき、"bar"を取得するには継続を使うことになる。 free applicativeだと両方取得できるので、たとえばエラーを全て集めるみたいな例だとapplicativeの方が便利。
nekketsuuu.icon モナドだと計算の順番が出来て引数の順番に依存しちゃうけど、アプリカティブだとそうじゃないみたいな話かな。
Free applicativeを拡張可能にしたい。
モナドとアプリカティブでプリミティブを分けたくない。
案1：EffApからEffへの変換を書く。
モナドの計算とアプリカティブの計算を型で分けられるけど、いちいち変換しないといけない。
案2：コンストラクタにImpureもImpureApも含めてしまう。
使いやすいけど、Applicativeの操作を型で保証できない。
たとえばアプリカティブで並列計算してたところでflat_mapしちゃう、とか。
案3：型パラメータに含めてしまう。
これだと弱点は型が複雑になることくらい……？
「この前思いついた所なのでまだあんまり考えられていない」
名前付き extensible effects
のでextensible effectsを使おう。
ただし：
推論されない：型リストからエフェクトの型を定めることができない。
clear :: (Monoid m, State m \in xs) => Eff xs () を作ろうとするとmが曖昧になる。
対応できない：同じ方を持つ複数のエフェクトを持てない。
たとえば [State Int, State Int]からどちらかを意図的に選択することができない。
再利用できない：mtlのクラスで定義された演算を再利用できない。
推論できる：State m \in xs に当たる制約をAssociate "S" (State m) xsみたいに書くことで実現。
functional dependencies
"S"は型レベル文字列（DataKinds）
対応できる：エフェクトをキーで指定できるのでOK。
再利用できる：mtlのインターフェースが使える。
いちいち手動で再定義する必要は無い。
nekketsuuu.icon 型レベルのリストが、型レベルの辞書に変わった感じ？
Effect{ive,ful} Cycle.js
Webフロントエンドのフレームワークは、以下の性質を満たしていてくれると嬉しい。
1. 種々の副作用を互いに分離できる。
異なる副作用は別々に処理したい。
関心の分離をしたい。
テスタビリティを上げたい。
後から副作用を追加できるようにしておきたい。
2. 非同期が織り込み済み。
これを解決するために：
副作用の処理をclient-serverモデルっぽく捉えて、client (DOMとかHTTPとか) が server (effect handler) に副作用 (effect) の処理を依頼する形に考えられないか。
Freer, More Extensible Effectsの図。
→異なる副作用を別々に処理する。
Observableが値を流し、Observerがその値を使って何をするかを決める。
→非同期が織り込み済み。
https://gyazo.com/6bfe054a1a167b0a9e4cffde49c9f785
componentはeffectfulな計算をする。
componentが持つeffectはdriver（やhigher-order component）によってhandleされる。
すべてのeffectをhandleできればアプリケーションが実行できる。
TypeScriptではどこでも副作用を書けてしまうのでアレだが、このフレームワークでは副作用の処理をdriverに書くことで、メインの処理をピュアに書ける。 nekketsuuu.icon 型では安全性を保証できなさそう……？
Cycle.js vs RxJS
Cycle.jsではStreamのライブラリを選べる。なのでStreamとしてRxJSを選ぶこともできる。
Cycle.jsはStreamのラッパー的存在。
Streamの扱い方の指針を与えるフレームワーク
Effective Rust
元ネタ：eff.lua
Rustにはスタックレスコルーチンがあるので、これを使ってoneshot algebraic effectが実装できる。
pull型で動く。
ハンドラは再開を通知する形。
ランタイムが継続を実行する。
そのまま書くと、Rustのlifetime checkerと相性が悪い。
performで呼ばれるhandlerの中で再びperformを呼びうるが、そうするとふたつのハンドラが同時に参照するので駄目。
Frankという言語で採用してるように、計算と値を区別して、引数の評価中に出たエフェクトを処理する形で書くと良い。 しかもこうすると、エフェクトハンドルがスタックを重ねるスタイルじゃなくてループを回すスタイルになるので速い。
Monads and Effects
注：call-by-value。
そもそもeffectとは。
ここでは：型システムの一種として捉える。
$ \Gamma \vdash M : A ! e みたいに、judgementにeffect $ eが付く。
直感：computationをしたときに、高々$ eというeffectが起きる。
たとえば基本的な型の導出を考えると、どんなeffectの見積もりになりそうか考えてみよう。
たとえば$ \vdash \langle M_1, M_2 \rangle : A \times B ! ここは何でしょう
他にもletとか関数適用とかラムダ抽象とか。
タプルとletに関しては、「effectがスタックする」みたいなのを考えれば良さそうだ。
例として、memory-state effectを考えてみる。
$ i番目のメモリセルに書く、読む、みたいな。
いくつかbase effectsがある。
exn: exception
div: divergence
ndet: non-determinism
alloc(h), read(h), write(h): memory operation
また、Kokaではeffectの順番は無視する。
base effectsを組み合わせて色々なeffectを作れる。
total ≡ 〈〉
pure ≡ 〈exn, div〉
st(h) ≡ 〈alloc(h), read(h), write(h)〉: memory-state h について何でもできるぜ
io ≡ 〈st(io), pure, ndet〉: 何でもできるぜ
Row-polymorphicっぽくeffectを扱っているのが面白い。
$ \langle exn | \mu \rangle
ところで、ラムダ抽象と関数適用はどう捉える？
関数の時点では、関数適用のeffectが発生しているとは考えたくない。
代わりに、関数自体にeffectが込められていると考えたい。
ので、関数型の矢印にeffectで添え字を付けて、「関数を呼び出したときにこのeffectが起こりうる」を表現する。
EffectはParametric Monadとして捉えられる。
たとえばHaskellのIOモナドにmemory-state effectが添え字として入ったのをイメージ。
モナドにおけるモナド則的なものはこの場合どういう規則になるだろう？
これを考えると、以下のようなことが分かる。
effectは「スタックする」という演算に対してモノイドになってる。
あくまで上からの見積もりで、preorderが入る。
Further topics
Semantics
Graded monad (for the formal semantics)
Recursion
Algebraic effects and effect handlers
Effect inference
Polymorphic effect
Q. exnに型パラメーターを入れられる？（たとえばOCamlのexceptionみたいに）
A. Kokaには多分無い
Q. たとえばexnに型パラメーターを持たせると、effect inferenceが多相再帰みたいになって推論不能になったりしそう。
Q. effect情報を使ったコンパイルは考えられている？ たとえばexnが無ければ例外処理消せる、とか。
A. Kokaはしてないと思うが、そういう研究はある。たとえば実行にかかるコストをeffectとして見積もるとか。メモリアクセスがdistinctになっている情報がeffectから分かるのでそれを使って並列化可能性を見積もるとか。
How do you implement Algebraic Effects?
nekketsuuu.icon スライドが分かりやすい……。
低レベルで実装する。
effect invocation ： longjmp
effect handler ： stackframe + ip
continuation ： stackframe + ip
様々な言語から呼び出せて速いけど、実装が大変。バックエンド向け？
effect invocation ： yield
effect handler ： create & resume
continuation ： coroutine
ただしcoroutineをコピーするような操作が無いと、continuationがoneshotに限定される。
continuationは何回も呼び出したいものなのに、coroutineは状態をコピーできない。
effect operation ： prompt tag
effect invocation ： shift-at
effect handler ： reset-at
continuation ： continuation
Multiprompt shift/reset：普通のshift/resetだとshiftから一番近いpromptまで飛ぶが、multiprompt shift/resetではそれぞれのpromptにタグをつけておくことでshift時に飛びたいpromptを指定できる。
ただしタグはglobalじゃない。
shift-atを重ねるとネストする。
effect invocation ： Impure
effect handler ： run
continuation ： bindの右辺
Double-barrelled CPS：continuationをふたつ持つ。CPS+exception。
これを拡張して、CPS+algebraic effectsに対応して(1+n)個の継続を持つものを考えれば良いのでは？
この論文と同じ話になるかも？
Effective Idris: Effects
Idrisの標準ライブラリにあるEffectsの話。 code:idris
Effect : Type
Effect = (x : Type) -> Type -> (x -> Type) -> Type
data EFFECT : Type where
MkEff : Type -> Effect -> EFFECT
Effect = 返り値 * リソース * リソースの更新。
Idrisには依存型があるのでリソースが更新されうる。
EFFECT = パラメータ * Effect。
nekketsuuu.icon 依存型があることによって何が変わっているかに注目して読むと見通し良さそう。
Row-based type systems for algebraic effect handlers
handler-not-found errorを事前に防ぎたい。
Row-based effect system (Hillerström+ 2016, ...)
特徴
例：to-maybe : ∀α. (unit -> <fail> α) -> <> α option
このままだと、to-maybeに与える関数として、effectがfailしか起こらないものしか扱えない。
ので、row-polymorphismを使うことで他のeffectがあることを許す。
to-maybe : ∀α. (unit -> <fail | ρ> α) -> <| ρ> α option
型上でeffectの複製ができる。
<fail, int choose, fail> とか書ける。
<int choose, bool choose> みたいに書いて、ハンドラでは int choose -> ... みたいに書ける。
ただしこう書くと順番があって、先に int choose をハンドルしないといけない。
この仕組みがあるとsubtypingが無くても結構リッチな型が書けるのでeffect systemが単純になる。
effectの抽象化がやりやすくなる。
nekketsuuu.icon レコードのrow-polymorphismと似ているが、レコードみたいなラベルは無くて順番があるというのがちょっぴり違う。
continuationと機能としては似ているのだけど、effect systemという側面から見ると面白さがあって良さ。
OCamlのラベル引数の体系は「名前が違うと順番は気にしないが、名前が同じだと順番を気にする」という意味で似てる、という話。
懇親会
nekketsuuu.icon 話した中で記録に残しておきたいものを。
僕「oneshotのalgebraic effectってどのくらいデメリットあるんですか」
multishotであってほしいものって、リストにmapするときのfとか、非決定的に何回か計算が必要なときとか。
要するに任意回必要な場合。
なので、使い方によってはoneshotであまり困らない。
ややポジショントークかもしれない。
こういうのはoneshot制約がかかっている論文には（査読を通すために）色々書いてあるので読むと良い。
ファイルをreadして、closeをちょうど1回だけしたいときとか、oneshotの方がたすかることもある。
これはポジショントークっぽい。
線形型やアフィン型で解決したい問題っぽい。
algebraic effectを継続だと思うと、継続が役に立つ場面であるバックトラックをする場面では、oneshotだと困る。
effectをpolymorphicにするときに、effectの方に型変数をつけるか、effectの型の方に型変数をつけるかでeffect推論の難易度が変わる。
正確には、型アノテーションをつけるかつけないか？
∀α. α e :: α → α と e :: ∀α. α → α
後者だと handle :: Λα. ...って感じでハンドラの中で型を受け取って色々することになる。
だからハンドラの中では (+) とか使えない。
value restrictionが無くても、ハンドラのbodyを制限すると上手くやれるよって話。